Definitions | t T, #$n, x:A. B(x), A B, n+m, a<b, Void, x:A B(x), P  Q, False, A, , {x:A| B(x) }, , data(T), Atom$n, left+right, Type, x:A B(x), {i..j }, <a,b>, Prop, True, i j, b,  b, , s = t, P & Q, i j < k, f(a), x.A(x),  x. t(x), 1of(t), i= j, f[x:=v], i< j, T, P  Q, P  Q, Unit, encrypt(tab;keyv), secret-table(T), Id |